CI summary for 2150652:

• All 6 Cygwin/MinGW trunk workflows failed with a version mismatch, since trunk is now 5.3
• linux-arm64-5.2 aborted domain_spawntree with Fatal error: Failed to create domain [ocaml5-issue] Fatal error: Failed to create domain on s390x, MinGW, Cygwin, ... #428

Out of 59 workflows 7 failed with 1 genuine failure and 6 ci setup issues

I've rebased the PR on main after the merge of #429

CI summary for 024dd85

• 4 workflows aborted domain_spawntree with Fatal error: Failed to create domain [ocaml5-issue] Fatal error: Failed to create domain on s390x, MinGW, Cygwin, ... #428
  • Cygwin 5.2
  • Cygwin trunk
  • FP trunk
  • MinGW 5.2
• MinGW bytecode 5.2 timed out during threadomain [ocaml5-issue] Windows failures on threadomain #203

Out of 44 workflows 5 failed with all 5 being genuine failures.

On the other hand, despite its downsides the old Lin test has also managed to stress the runtime into triggering defects #412

Do you think the STM tests are less likely to trigger such defects?

Thanks for the review!

Discussing this PR with you triggered me to look up previous counterexamples reported by the Lin Out_channel test.
Indeed, the last merge to main a571972 triggered, e.g., the following for the Linux 5.2 debug workflow:

Messages for test Lin Out_channel test with Domain:

  Results incompatible with sequential execution

                                           |                  
                         Out_channel.output_byte t 2 : Ok (())
                                           |                  
                       .--------------------------------------.
                       |                                      |                  
         Out_channel.length t : Ok (1)         Out_channel.close_noerr t : ()   

This should have a possible sequentialization (below) which we seem to miss:

Out_channel.output_byte t 2;;
Out_channel.length t;;
Out_channel.close_noerr t;;

Looking at previous counterexamples also made me realize that

• some of them are triggered by using close/close_noerr in parallel. However we won't generate such inputs in this STM test version ATM unfortunately, because they don't have a well-balanced open-close serialization. I want to experiment with lifting this limitation.
• other Lin Out_channel counterexamples are triggered by weird output unlinearizable behaviours arising from running other cmds on already closed channels. This is a gray-zone specification-wise, which does not offer an immediate benefit AFAICS. As such, I'm more reluctant to invest in lifting it.

                                                                                                                   |                                                       
                                                                                                     Out_channel.flush t : Ok (())                                         
                                                                 Out_channel.output_bytes t "7)\016)\170\245A{(2\255\000mr\185\243\206\2475-\192i\135\2216}w" : Ok (())    
                                                                                             Out_channel.set_binary_mode t false : Ok (())                                 
                                                                                                                   |                                                       
                                                           .---------------------------------------------------------------------------------------------------------------.
                                                           |                                                                                                               |                                                       
                                             Out_channel.length t : Ok (27)                                                                                  Out_channel.close_noerr t : ()                                        
                                         Out_channel.is_buffered t : Ok (true)                                                                               Out_channel.close t : Ok (())                                         
                                         Out_channel.output_byte t 6 : Ok (())                                                                               Out_channel.pos t : Ok (65536)                                        
                                                                                                                                                         Out_channel.is_buffered t : Ok (true)                                     
                                                                                                                                     Out_channel.output_bytes t "K\226" : Error (Sys_error("Bad file descriptor"))                 
                                                                                                                                                         Out_channel.is_buffered t : Ok (true)                                     
                                                                                                                     Out_channel.output_substring t "\197\180\2484g\180\230\193" 4 7 : Error (Invalid_argument("output_substring"))
                                                                                                                                                             Out_channel.flush t : Ok (())                                         
  

Our discussion also made me check my recollection regarding locking:
https://github.com/ocaml/ocaml/blob/cedff5854ac91dccf5847b527192223ef506b1e2/runtime/io.c#L60

All operations on channels first take the channel lock.

As such, they Out_channel operations should act atomically when used in parallel and be sequential consistent.

On the other hand, despite its downsides the old Lin test has also managed to stress the runtime into triggering defects #412

Do you think the STM tests are less likely to trigger such defects?

Possibly, but I'm unsure.

• A single Lin input will call the Out_channel interface (up to) 50 times * 1 parallel run * #interleavings times.
• In comparison a single STM input will call the interface (up to) 25 times * 1 parallel run.

Since #interleavings can be quite high, a corner case bug is more likely to trigger more often when it is run more.
On the other hand, when considering this behaviour across a count of 1000, the negative Lin test will finish sooner (and report a "counterexample") whereas the current STM test runs to completion (1000 inputs * 25 repetitions).

In 8236876 I extend the STM tests to be able to generate close and close_noexn in state Closed too.

This should have a possible sequentialization (below) which we seem to miss:

In the sequentialized version, the length will most probably be 0, as the buffer is not flushed; the output we see is due to the close_noerr being half-run, having flushed but not closed yet (as those two steps are explicitly not run atomically), isn’t it?

This is a gray-zone specification-wise, which does not offer an immediate benefit AFAICS.

To make sure that I understand correctly what this is doing, because I think I missed it in my first review: due to the postcond function, we’ll never test close or close_noerr in one of the parallel branches except when the other branch is only doing open and close calls, or am I mistaken in how postcond is used in all_interleavings_ok? This would mean those tests would never run into issues such as ocaml/ocaml#11878 I suppose?

This should have a possible sequentialization (below) which we seem to miss:

In the sequentialized version, the length will most probably be 0, as the buffer is not flushed; the output we see is due to the close_noerr being half-run, having flushed but not closed yet (as those two steps are explicitly not run atomically), isn’t it?

This is a probable explanation indeed! 👍
However it seems a bit unsatisfying that this stops testing and is reported as a counterexample of parallelism-safety.

This is a gray-zone specification-wise, which does not offer an immediate benefit AFAICS.

To make sure that I understand correctly what this is doing, because I think I missed it in my first review: due to the postcond function, we’ll never test close or close_noerr in one of the parallel branches except when the other branch is only doing open and close calls, or am I mistaken in how postcond is used in all_interleavings_ok? This would mean those tests would never run into issues such as ocaml/ocaml#11878 I suppose?

Point well taken - and yes, you are right 👍
Following the Erlang version described in the ICFP'09 paper, STM will generate candidate "Y"-triples and only keep those which satisfy all preconditions in all interleavings (which is what all_interleavings_ok should express). This indeed leaves out two parallel close* cmds.

I've therefore taken a pass over the STM test and extended the cmds so that all of them can also occur in state Closed. The only generator and precond limitation now is that Open_text is not allowed in state Open (this was also a limitation of the Lin test).

This revealed a divergence from the spec as I shared offline:

val close : t -> unit
(** Close the given channel, flushing all buffered write operations.  Output
    functions raise a [Sys_error] exception when they are applied to a closed
    output channel, except {!close} and {!flush}, which do nothing when applied
    to an already closed channel.  Note that {!close} may raise [Sys_error] if
    the operating system signals an error when flushing or closing. *)

Yet output_string, output_bytes, output, and output_substring of length 0 on a Closed channel does not fail, e.g.:

--- Failure --------------------------------------------------------------------

Test STM Out_channel test sequential failed (22 shrink steps):

   Close
   Output_string ""


+++ Messages ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Messages for test STM Out_channel test sequential:

  Results incompatible with model

   Close : Ok (())
   Output_string "" : Ok (())

For now, I've adjust postcond to accept these cornercases.
We should consider submitting a PR to adjust the specification though...

This would mean those tests would never run into issues such as ocaml/ocaml#11878 I suppose?

We can now experimentally confirm that the latest changes can indeed find issues like that.
All 5.2 and 5.3/trunk workflows show a regression on outputting on a closed Out_channel, where only the first cmd now triggers an exception: 😮

+++ Messages ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Messages for test STM Out_channel test sequential:

  Results incompatible with model

   Close_noerr : Ok (())
   Output_string "}\169)gN\255\017" : Error (Sys_error("Bad file descriptor"))
   Output_byte 48 : Ok (())

Some overdue CI summaries...

For 9c63209:

• Cygwin trunk aborted during domain_spawntree [ocaml5-issue] Fatal error: Failed to create domain on s390x, MinGW, Cygwin, ... #428
• MinGW bytecode 5.1 crashed during threadomain [ocaml5-issue] Windows failures on threadomain #203
• MinGW bytecode 5.2 aborted during domain_spawntree [ocaml5-issue] Fatal error: Failed to create domain on s390x, MinGW, Cygwin, ... #428
• MinGW trunk aborted during domain_spawntree [ocaml5-issue] Fatal error: Failed to create domain on s390x, MinGW, Cygwin, ... #428
• macOS trunk failed to build dune [dune-issue] dune fails build under trunk/5.3 on macOS #433
• Cygwin 5.2 was cancelled after 138m during Dynlink [ocaml5-issue] Deadlock in Dynlink test on Cygwin+MinGW+MSVC #307

Out of 44 workflows 5 failed and 1 was cancelled, all 6 due to genuine issues

For 8236876:

• Cygwin 5.2 aborted during domain_spawntree [ocaml5-issue] Fatal error: Failed to create domain on s390x, MinGW, Cygwin, ... #428
• Cygwin trunk aborted during domain_spawntree [ocaml5-issue] Fatal error: Failed to create domain on s390x, MinGW, Cygwin, ... #428
• MinGW 5.2 aborted during domain_spawntree [ocaml5-issue] Fatal error: Failed to create domain on s390x, MinGW, Cygwin, ... #428
• MinGW bytecode trunk aborted during domain_spawntree [ocaml5-issue] Fatal error: Failed to create domain on s390x, MinGW, Cygwin, ... #428
• macOS trunk failed to build dune [dune-issue] dune fails build under trunk/5.3 on macOS #433

Out of 44 workflows 5 failed with all 5 being genuine issues

For 0c8fdcb:

• MinGW bytecode 5.1 timed out in threadomain [ocaml5-issue] Windows failures on threadomain #203
• 4 workflows aborted during domain_spawntree [ocaml5-issue] Fatal error: Failed to create domain on s390x, MinGW, Cygwin, ... #428
  • Cygwin 5.2
  • Cygwin trunk
  • MinGW 5.2
  • macOS 5.2
• macOS trunk failed to install dune [dune-issue] dune fails build under trunk/5.3 on macOS #433
• MinGW 5.1 failed the new STM Out_channel test with flush raising Sys_error("Bad file descriptor") when used in parallel
• all 21 5.2 and trunk/5.3 workflows failed the new STM Out_channel due to the exception regression [ocaml5-issue] Output to closed Out_channel fails to raise Sys_error #432
  • 32bit 5.2
  • 32bit trunk
  • Bytecode 5.2
  • Bytecode trunk
  • Cygwin 5.2
  • Cygwin trunk
  • FP 5.2
  • FP trunk
  • Linux 5.2
  • Linux 5.2 debug
  • Linux trunk
  • Linux trunk debug
  • MinGW 5.2
  • MinGW bytecode 5.2
  • MinGW bytecode trunk
  • MinGW trunk
  • macOS 5.2
  • linux-arm64-5.2
  • linux-s390x-5.2
  • linux-ppc64le-5.2
  • macos-arm64-5.2

Out of 44 workflows 24 failed with a total of 28 failures (4 workflows failed two tests) with all of them being genuine

The PR's latest test revision is so effective at triggering the #432 regression that we should consider temporarily relaxing the test to accept the current behaviour, to avoid having to check ~20 failing workflows on each CI run... 😬

I rebased on main to avoid more false alarms and added 86f2ab2 to temporarily disable the #432 regression reports.

CI summary:

• Cygwin 5.2 timed out during the Lin Dynlink test [ocaml5-issue] Deadlock in Dynlink test on Cygwin+MinGW+MSVC #307
• macOS trunk failed to build dune [dune-issue] dune fails build under trunk/5.3 on macOS #433

Out of 44 workflows 2 failed, with both being genuine issues

CI summary for merge to main:

• macOS trunk failed to build dune [dune-issue] dune fails build under trunk/5.3 on macOS #433

Out of 45 workflows 1 failed with a genuine issue